T:Type, P:((T List)prop{i:l}), L:(T List), x:T.
((L1:T List. (iseg(T; L1; append(L; cons(x; [])))  P(L1)))
 ((L1:T List. (iseg(T; L1; L)  P(L1)))))
 (P(append(L; cons(x; [])))  ((L1:T List. (iseg(T; L1; L)  P(L1))))) 

latex

Definitions	t  T, prop{i:l}, x(s), x:A. B(x), iseg(T; l1; l2), P  Q, x:A. B(x), A, append(as; bs), P  Q, P  Q, P  Q, P  Q, False, ||as||, True, T, b
Lemmas	iseg weakening, iseg nil, cons iseg, squash wf, true wf, iseg append iff, append wf, not wf, iseg wf